Aspects of Incompleteness: Chapter 1 読書録3
次:
Memo
$ \varphiが$ \xi(x)の$ T上不動点であるとは,$ T \vdash \varphi \leftrightarrow \xi(\varphi)となることである a. 任意の$ \Gamma^+論理式$ \gamma(x)に対して
$ \mathbf{Q} \vdash \varphi \leftrightarrow \gamma(\varphi)となる$ \varphiが$ \Gamma^+文として実行的に取れる.
proof of a
$ x \equiv v_mとする
$ \delta(x) \equiv \exists z \lbrack \mathrm{Subst_1}(m,x,x,z) \land \gamma(z) \rbrackとする.
このとき$ \mathbf{Q} \vdash \mathrm{Subst_1}(m,\delta,\delta,z) \leftrightarrow z = \delta(\delta)だから
$ \delta(\delta) \equiv \exists z\lbrack \mathrm{Subst}(m,\delta,\delta,z) \land \gamma(z) \rbrackであるから$ \mathbf{Q} \vdash \delta(\delta) \leftrightarrow \gamma(\delta(\delta))となる.
$ \delta(\delta) \equiv \varphiとすれば所望の$ \Gamma^+文が取れる.
精密な議論
$ x \equiv v_mとする
$ \delta(x) \equiv \exists z \lbrack \mathrm{Subst_1}(m,x,x,z) \land \gamma(z) \rbrack
このとき$ \mathbf{Q} \vdash \mathrm{Subst_1}(m,\ulcorner \delta \urcorner, \overline{\ulcorner \delta \urcorner}, z) \leftrightarrow z = \overline{\ulcorner \delta( \overline{ \ulcorner \delta \urcorner}) \urcorner}
$ \delta(\overline{\ulcorner \delta \urcorner}) \equiv \exists z \lbrack \mathrm{Subst_1}(m,\overline{\ulcorner \delta \urcorner},\overline{\ulcorner \delta \urcorner},z) \land \gamma(z) \rbrack
だから
$ \mathbf{Q} \vdash \delta(\overline{\ulcorner \delta \urcorner}) \leftrightarrow \exists z \left\lbrack z= \overline{\ulcorner \delta( \overline{ \ulcorner \delta \urcorner}) \urcorner} \land \gamma(z) \right\rbrack
$ \mathbf{Q} \vdash \delta(\overline{\ulcorner \delta \urcorner}) \leftrightarrow \gamma(\overline{\ulcorner \delta( \overline{ \ulcorner \delta \urcorner}) \urcorner})
このとき$ \delta(\overline{\ulcorner \delta \urcorner}) \equiv \varphiとすれば所望の$ \Gamma^+文となる.
$ \mathbf{Q} \vdash \varphi \leftrightarrow \gamma(\overline{\ulcorner \varphi \urcorner})
b. 任意の$ \Gamma^+論理式$ \gamma(x,y)に対して
$ \mathbf{Q} \vdash \xi(x) \leftrightarrow \gamma(x, \xi)となる$ \xi(x)が$ \Gamma^+文として実行的に取れる.
proof of b
$ x \equiv v_m,y \equiv v_nとする
$ \eta(x,y) \equiv \exists z \lbrack \mathrm{Subst_1}(n,y,y,z) \land \gamma(x,z) \rbrackとする
このとき$ \mathbf{Q} \vdash \mathrm{Subst_1}(m,\eta,\eta,z) \leftrightarrow z = \eta(x, \eta)
$ \mathbf{Q} \vdash \eta(x,\eta) \leftrightarrow \gamma(x,\eta(x,\eta))となる
$ \eta(x,\eta) \equiv \xi(x)とすれば$ \mathbf{Q} \vdash \xi(x) \leftrightarrow \gamma(x,\xi)となってよい.
c. 任意の$ \Gamma^+文$ \gamma_0(x,y), \gamma_1(x,y)に対して次の$ \Gamma^+文$ \varphi_0,\varphi_1を実行的に取ってこれる
$ \mathbf{Q} \vdash \varphi_0 \leftrightarrow \gamma_0(\varphi_0,\varphi_1)
$ \mathbf{Q} \vdash \varphi_1 \leftrightarrow \gamma_1(\varphi_0,\varphi_1)
proof of c
$ x \equiv v_m,y \equiv v_n,$ i = 0,1とする
$ \delta_i(x,y) \equiv \exists z_0,z_1 \lbrack \mathrm{Subst_2}(m,x,n,y,x,z_0) \land \mathrm{Subst_2}(m,x,n,y,y,z_1) \land \gamma_i(z_0,z_1) \rbrackと定める.
これらを思い出す
$ \mathbf{Q} \vdash \mathrm{Subst_2}(m,\delta_0,n,\delta_1, \delta_0, z_0) \leftrightarrow z_0 = \delta_0(\delta_0,\delta_1)
$ \mathbf{Q} \vdash \mathrm{Subst_2}(m,\delta_0,n,\delta_1, \delta_1, z_1) \leftrightarrow z_1 = \delta_1(\delta_0,\delta_1)
$ \mathbf{Q} \vdash \delta_i(\delta_0,\delta_1) \leftrightarrow \gamma_i(\delta_0(\delta_0,\delta_1), \delta_1(\delta_1,\delta_1))となるので
$ \delta_0(\delta_0,\delta_1) \equiv \varphi_0$ \delta_1(\delta_0,\delta_1) \equiv \varphi_1とすれば所望のものとなる
$ \mathbf{Q} \vdash \varphi_0 \leftrightarrow \gamma_0(\varphi_0,\varphi_1)
$ \mathbf{Q} \vdash \varphi_1 \leftrightarrow \gamma_1(\varphi_0,\varphi_1)
d. 任意の$ \Gamma^+論理式$ \gamma(x,y)に対して
$ \mathbf{Q} \vdash \xi(k) \leftrightarrow \gamma(k,\xi(k))となる$ \Gamma^+論理式$ \xi(x)を任意の$ \rm kに対して実行的に取ってこれる
proof of d
$ x \equiv v_m,y \equiv v_nとする
$ \eta(x,y) \equiv \exists z \lbrack \mathrm{Subst}_2(m,x,n,y,y,z) \land \gamma(x,z) \rbrackとする
$ \mathbf{Q} \vdash \mathrm{Subst_2}(m,k,n,\eta,\eta, z) \leftrightarrow z = \eta(k,\eta)
したがって$ \mathbf{Q} \vdash \eta(k,\eta) \leftrightarrow \gamma(k,\eta(k,\eta))だから
$ \xi(x) \equiv \eta(x,\eta)とすれば所望のものとなる
e. $ Tは$ \bf PA拡大理論とする.任意の$ \Gamma^+論理式$ \gamma(x,y)に対して
$ \mathbf{PA} \vdash \xi(x) \leftrightarrow \gamma(x,\xi(\dot{x}))となる$ \Gamma^+論理式$ \xiを取ってこれる
proof of e
$ \eta(x,y) \equiv \gamma(x, \mathrm{subst}_2(m,x,n,y,y))と定める.
$ \mathbf{PA} \vdash \mathrm{subst_2}(m,x,n,\eta,\eta) = \eta(\dot{x},\eta)が得られる
$ \mathbf{PA} \vdash \eta(x,\eta) \leftrightarrow \gamma(x,\eta(\dot{x},\eta))となる
$ \xi(x) \equiv \eta(x,\eta)とすれば所望のものとなる
精密な議論
$ x \equiv v_\mathrm{m},y \equiv v_\mathrm{n}とする
$ \eta(x,y) \equiv \gamma(x, \overline{\ulcorner \mathrm{subst}_2(\mathrm{m},\mathrm{x},\mathrm{n},\mathrm{y},\mathrm{y}) \urcorner})とする
$ \begin{aligned} \mathrm{subst_2}(\mathrm{m,x,n}, \ulcorner \eta \urcorner,\ulcorner \eta \urcorner) &= \mathrm{subst}_1(\mathrm{m,x},\mathrm{subst}_1(\mathrm{n},\ulcorner \eta \urcorner,\ulcorner \eta \urcorner)) \\&= \mathrm{subst_1}(\mathrm{m,x},\ulcorner \eta(v_\mathrm{m},\ulcorner \eta\urcorner) \urcorner) \\&= \ulcorner \eta(x,\ulcorner \eta \urcorner) \urcorner \end{aligned}
$ \mathbf{PA} \vdash \overline{\ulcorner \mathrm{subst}_2(\mathrm{m,x,n},\ulcorner \eta \urcorner,\ulcorner \eta \urcorner) \urcorner} = \overline{\ulcorner \eta(x,\overline{\ulcorner \eta \urcorner}) \urcorner}
$ \mathbf{PA} \vdash \eta(x,\overline{\ulcorner \eta \urcorner}) \leftrightarrow \gamma(x, \overline{\ulcorner \eta(x, \overline{\ulcorner \eta \urcorner}) \urcorner})
$ \xi(x) \equiv \eta(x,\overline{\ulcorner \eta \urcorner})とすれば$ \mathbf{PA} \vdash \xi(x) \leftrightarrow \gamma(x, \overline{\ulcorner \xi(x) \urcorner})となって良い.
Memo
他にも様々な不動点の構成がある.
$ \gamma(x,y)として$ \mathbf{Q} \vdash \theta \leftrightarrow \gamma(\theta,\lnot\theta)となる$ \thetaを作りたいとする.
$ \mathbf{Q} \vdash \nu(\varphi,y) \leftrightarrow y = \lnot \varphiとなる$ \nu(x,y)が$ \varphiに対して存在する
$ \delta(x) \equiv \exists y \lbrack \nu(x,y) \land \gamma(x,y) \rbrackとすると不動点補題より$ \mathbf{Q} \vdash \theta \leftrightarrow \delta(\theta)となる$ \thetaが存在する.
$ \begin{aligned}\delta(\theta) &\equiv \exists y \lbrack \nu(\theta,y) \land \gamma(\theta,y) \rbrack \\ &\equiv \exists y \lbrack y = \lnot\theta \land \gamma(\theta,y) \rbrack \end{aligned}
であるから$ \mathbf{Q} \vdash \theta \leftrightarrow\gamma(\theta,\lnot\theta)となってOK
今後不動点補題はかなり省略して使う.
($ \xiが$ \Gamma^+論理式だとして)「$ \varphiを$ \bf Q \vdash \varphi \leftrightarrow \xi(\varphi)として取る」と言った場合,それは「$ \varphiを$ \bf Q \vdash \varphi \leftrightarrow \xi(\varphi)となる不動点を$ \Gamma^+文として取ってくる」と言う意味である
Memo
理論$ Sが決定不能であるとは,$ \mathrm{Th}(S)が再帰的であることを指す. $ TはRobinson算術の無矛盾拡大理論とする.$ \mathrm{Th}(T)を$ T上で表現する論理式は存在しない. proof
$ \mathrm{Th}(T)を$ T上で表現する論理式$ \tau(x)が存在するとする.
$ \tauを使って次のような不動点$ \varphiを考える.
$ \mathbf{Q} \vdash \varphi \leftrightarrow \lnot \tau(\varphi)
この$ \varphiは$ Tで証明可能か?
$ T \vdash \varphiとする:すなわち$ \varphiは$ Tの定理だとする.
$ \tau(x)の表現性より$ T \vdash \tau(\varphi)でなければならない.
しかし$ \varphiの不動点の定義として,このとき$ T \vdash \lnot \varphiとなってしまう.
$ T \nvdash \varphiだとする:すなわち$ \varphiは$ Tの定理ではないとする.
$ \tau(x)の表現性より$ T \vdash \lnot \tau(\varphi)となければならない.
すると不動点としての定義より$ T \vdash \varphiとなって元々の過程に反しておかしい.
proof
仮に$ \bf Qの拡大理論$ Tが決定可能であったとする.
すなわち$ \mathrm{Th}(T)が再帰的関係であったとする. このときCor 1.1.aより$ \mathrm{Th}(T)は$ \bf Q上で表現可能であり,$ T上でも表現可能となる.
しかしLem2より実際には表現不能だから,おかしい.
Def
$ Uに対し,任意の$ \varphiで$ U \vdash \varphi \leftrightarrow \mathrm{Tr}(\varphi)となる$ \mathrm{Tr}(x)を真理定義述語という. $ \bf Qの無矛盾拡大理論$ Uの真理定義述語は構成できない. proof
もし存在するとしたら不動点補題より$ \mathbf{Q} \vdash \varphi \leftrightarrow \lnot \mathrm{Tr}(\varphi)となる不動点を取ってこれる.
この不動点がどういう帰結をもたらすかは明らかであろう.
Memo
ただしThm1.3は部分的に定義する述語は定義できる.
論理式のクラス$ \Gammaに対しての部分的な真理定義述語$ \mathrm{Tr}_\Gamma(x)を次のように定める 任意の$ \Gamma文$ \varphiに対して$ T \vdash \varphi \leftrightarrow \mathrm{Tr}_\Gamma(\varphi)
このとき$ \mathbf{PA} \vdash \Gamma(x) \to \Gamma^d(\lnot x)
及び$ \Gamma \sube \Gamma'のとき$ \mathrm{PA} \vdash\Gamma(x) \to \Gamma'(x)
a. $ \Gamma論理式$ \mathrm{Sat}_\Gamma(x,y)が存在して次を満たす.
1. 任意の$ \Gamma論理式$ \gamma(x)に対して$ \mathbf{PA} \vdash \gamma(x) \leftrightarrow \mathrm{Sat}_\Gamma(x,\gamma)
2. $ \mathrm{Tr}_\Gamma(x) \equiv \mathrm{Sat}_\Gamma(0,x)とする.($ 0は$ v_0を意図している)
任意の$ \Gamma論理式$ \gamma(x)に対して$ \mathbf{PA} \vdash \gamma(x) \leftrightarrow \mathrm{Tr}_\Gamma(\gamma(\dot{x}))
したがって任意の$ \Gamma文$ \varphiに対して$ \mathbf{PA} \vdash \varphi \leftrightarrow \mathrm{Tr}(\varphi)
3. $ \mathbf{PA} \vdash \Gamma^d(x) \land \Gamma(y) \land \mathrm{Tr}_{\Gamma^d}(x) \land \mathrm{Tr}_\Gamma(x \to y) \to \mathrm{Tr}_\Gamma(y)
memoここにb.が存在するが,存在意義がわからないので一旦飛ばす.
b. $ \Delta_{n+1}論理式に対して$ \mathrm{Sat}_{B_n}(x,y)が存在して
任意の$ B_n論理式$ \beta(x)に対して$ \mathbf{PA} \vdash \beta(x) \leftrightarrow \mathrm{Sat}_{B_n}(x,\beta)
Memo
$ \gamma(x,y)を任意の$ \Gamma論理式とする.
このとき$ \Gamma論理式$ \xi(x)が存在して$ \mathbf{PA} \vdash \xi(k) \leftrightarrow \xi(k + 1) \lor \gamma(k,\xi)
これは次と同値$ \mathbf{PA} \vdash \xi(k) \leftrightarrow \mathrm{Tr}_\Gamma(\xi(k + 1) \lor \gamma(k,\xi))
d. $ \mathbf{PA} \vdash \Sigma_1(x) \land \mathrm{Tr}_{\Sigma_1}(x) \to \mathrm{Pr}_\mathbf{Q}(x)